x, y:Atom. (x =a y ~ ff)  ((x = y)) 

latex

Up	sqequal 1, sqequal 1
Definitions	t  T, x:A. B(x), P  Q, , P & Q, P  Q
Lemmas	atom sq, bfalse wf, assert of eq atom, not functionality wrt iff, assert of bnot, eqff to assert, iff transitivity, not wf, bnot wf, assert wf, bool wf